\documentclass[12pt,spanish]{book}
\usepackage[spanish,activeacute]{babel}
\usepackage[utf8]{inputenc}
\usepackage{framed}
\usepackage{anysize}
\usepackage{color}
\usepackage{wrapfig}
\usepackage{amsmath}
\usepackage{textcomp}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{fancyhdr}
\usepackage{cite}
\usepackage[pdftex]{graphicx}
\usepackage{epstopdf}
\usepackage{multirow}
\usepackage{xcolor}
\usepackage{listings}
\usepackage{caption}
\usepackage{tikz}
\usepackage{pdfpages}
\usepackage{amsmath}
\usepackage{shadethm}


\marginsize{3cm}{3cm}{2cm}{2cm}
\definecolor{shadecolor}{RGB}{238,238,238}
\definecolor{whitecolor}{RGB}{255,255,255}

\DeclareCaptionFont{white}{\color{white}}
\DeclareCaptionFormat{listing}{%
  \parbox{\textwidth}{\colorbox{gray}{\parbox{\textwidth}{#3}}\vskip-4pt}
}

\def\la{\left\langle\rule{0pt}{0em}}
\def\ra{\right\rangle}
\def\tab{\>\>\>\>\>\>\>\>\>\>\>\>}
\sloppy

\lhead[Sección \rightmark]{Sección \rightmark}
\chead[]{}
\rhead[\thepage]{\thepage}
\renewcommand{\headrulewidth}{0.5pt}

\fancypagestyle{plain}{
\fancyhead[L]{}
\fancyhead[C]{}
\fancyhead[R]{\thepage}
\fancyfoot[L]{}
\fancyfoot[C]{}
\fancyfoot[R]{}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}
}
\pagestyle{fancy}
\title{
\includegraphics[scale=0.2]{logo}
\line(1,0){350}\\
Universidad Nacional de Río Cuarto - FCEFQyN Departamento de Computación \\
		Proyecto Final(Cod. 1970)\\ 
		``Un Asistente para la especificación y verificación de propiedades temporales de Workflows''\\
		\line(1,0){350}\\
}
		
\author{
		Villar, Fernando\\
		D.N.I.: 33.814.181\\
		fernandovillar88@gmail.com\\
		\newline		
		\line(1,0){20}\\
		\newline\\
		\textbf{Director:} Dr. Regis, Germán 
}		


\begin{document}
\setlength{\parindent}{0pt}

\maketitle
\newpage
\section*{Resumen}
El área de modelado de procesos de negocios ha tenido gran auge en los últimos años como consecuencia, en parte, de la necesidad y demanda de eficiencia de un mundo cada vez más competitivo. Es por ello que existen actualmente numerosos trabajos cuyo objetivo es brindar soporte para tal fin; algunos ejemplos de ellos son [1] y [3].\\
Creemos importante la posibilidad de construir herramientas de software, o utilizar herramientas ya existentes, para asistir en la especificación y verificación de modelos de procesos de negocios. Localizamos nuestro interés fundamentalmente en métodos y lógicas que nos permitan modelar, analizar y verificar Procesos de Negocios.\\
Estamos trabajando en el análisis automático o semi-automático de modelos de Procesos de Negocios descriptos en lenguajes formales o semi-formales, como por ejemplo \emph{YAWL} [5]. Entre nuestros objetivos se encuentra la posibilidad de verificar propiedades que cumplen los mismos. Estas propiedades generalmente son caracterizadas por medio de distintas lógicas, en nuestro caso nos centraremos en la Lógica Temporal Lineal con Fluentes[6], cuya expresividad nos brindará la posibilidad de expresar de manera flexible propiedades complejas de modelos de Procesos de Negocios.\\
En el marco de este proyecto se pretende crear una herramienta que pueda ser capaz de interpretar los modelos realizados por YAWL, que permita además el uso de fluentes para complementar la definición de propiedades sobre los modelos interpretados. La herramienta realizará la interpretación de los modelos, la creación de propiedades y la validación de éstas de manera visual.

\newpage
\tableofcontents

\newpage
\input{chapters/chapter1}
  
\newpage
\input{chapters/chapter2}

\newpage
\input{chapters/chapter3}

\newpage
\input{chapters/chapter4}

\newpage
\input{chapters/chapter5}

\newpage
\chapter{Caso de estudio}
\noindent
\linebreak
En esta sección se tomará una situación de ejemplo para demostrar el funcionamiento de la herramienta desarrollada. El modelo que seleccionamos será tomado de los modelos que forman parte de los casos de estudio distribuído con la herramienta \emph{YAWL} y que suponen una complejidad suficiente para el análisis de workflows con una amplia diversidad de elementos y escenarios. Dicho modelo será descripto y se lo someterá a diferentes operaciones con el objetivo de verificar propiedades sobre él. Diferentes procesos no se podrán visualizar puesto que estos mismo ocurren de manera oculta a la interfaz propuesta para la herramienta, pero en los diferentes momentos se detallará qué es lo que ocurrió y por qué.

\section{Modelo}
El workflow seleccionado pertenece a un workflow general que modela el proceso seguido por una empresa de logística para la distribución de encomiendas. Mas precisamente, abordamos el sub-proceso de selección del tipo de transporte denominado \emph{Carrirer Appointment}. El mismo  representa el proceso de realizar una orden de envío de un pedido desde el momento que se realiza los preparativos del trasporte hasta la guía de transporte es confeccionada.

\begin{figure}[htp]
\centering
\includegraphics[scale=0.6]{images/modelStudy.png}
\caption{\textit{Modelo de estudio elegido}}
\end{figure}

Este modelo, tiene la característica de poseer sub-procesos los cuales representan la disponibilidad de si el trasporte de la orden sera realizada por un por un camión de carga o un vehículo de menor carga que éste. Según sea el caso se realizara un proceso correspondiente. De esta manera se cuenta con el proceso general de organizar el trasporte de la orden y estos dos últimos procesos mas simples para la preparación de la carga según el tamaño de la misma.\\
\linebreak 

Otra característica de este modelo es la parecencia de las regiones de cancelación. Las regiones de cancelación, como se comentó en el Capítulo 2, modelar la interferencia entre diferentes elementos del modelo. En el caso del modelo se tiene la tarea \textit{Time Out} que en caso de ejecutarse todo el proceso de de preparación de la carga, el elección de la ruta y los recursos para la misma se verán interrumpidos. Por otra parte si se finaliza con la tarea \textit{Prepare Trans Quote} se interrumpe el flujo de ejecución de la tarea \textit{Time Out} invalidado la posibilidad de cancelar el pedido. De esta manera se controla que el pedido se pueda cancelar haciendo que los costos no sean relevantes. En la Figura 6.3 se puede observar gráficamente la región afectada por la tarea \emph{Time Out}.

\begin{figure}[htp]
\centering
\includegraphics[scale=0.6]{images/cancellationModel.png}
\caption{\textit{Región de cancelación del caso de estudio}}
\end{figure}

\section{Escenarios de ejemplo}
Una vez ya cargado el modelo en la aplicación y habiendo interpretados cada uno de los elementos se procederá a definir tres situaciones o ejemplos del uso del modelo elegido. Por un lado se definirá una propiedad la cual no sea valida de manera de lograr un contraejemplo utilizando las funcionalidades de \emph{FWLA} y por el otro se utilizara los fluentes como mecanismo complementario a la definición de propiedades y se analizará el resultado. Para este último escenario se presentan los dos casos posibles. una propiedad válida y otra inválida.\\\newline

A continuación se presentara un caso en el cual se define una propiedad denominada ``exactly'' el cual expresa que dicho evento tiene que presentase o ``ejecutarse'' tan solo una vez. Esta propiedad queda definida sobre la herramienta como lo muestra la siguiente figura.\\


\begin{figure}[htp]
\centering
\includegraphics[scale=0.7]{images/propertyViolated.png}
\caption{\textit{Propiedad definida ``exactly''}}
\end{figure}

Teniendo esta propiedad definida sobre el modelo y el evento elegido para esta es ``time\_out.start''. El resultado de validar la misma mediante \textit{LTSA} es el siguiente.
 
\begin{figure}[htp]
\centering
\includegraphics[scale=0.5]{images/violationTrace.png}
\caption{\textit{Traza del violación de propiedad}}
\end{figure}

En la imagen 6.5 se puede ver que la propiedad no fue correcta puesto que el \emph{model checker} detecto un traza de ejecución que la hace invalida.\newline

La traza procesada genera la ejecución de estados traducidos al lenguaje original del modelo. Para este ejemplo se puede ver la siguiente traza de ejecución que hace invalida la propiedad de que sólo se ejecuta una vez el evento ``time\_out.start'', puesto que no se ejecuta en ninguno de los siguientes estados.

\begin{itemize}
  \item[1) ] Calculate\_time\_out
  \item[2) ] Preparte\_route\_guide
  \item[3) ] Prepare\_trans\_quote
  \item[4) ] Estimate\_usage
  \item[5) ] Less\_than\_truck\_load
  \item[6) ] Less\_than\_truck\_load.Prepare\_lt\_truck\_load
  \item[7) ] Less\_than\_truck\_load.Create\_bill\_of\_lading
  \item[8) ] Produce\_shipment\_notice
\end{itemize}
  
Aplicando estos traza conseguida en el modelo original se puede ver la falsedad de la propiedad de manera gráfica.

\begin{figure}[htp]
\centering
\includegraphics[scale=0.4]{images/violationTraceOnDiagram.png}
\caption{\textit{Traza del violación de propiedad en el diagrama}}
\end{figure}

Para el siguiente ejemplo se utilizará un fluente con el objetivo de aprovechar el poder expresivo de los mismos. Sin embargo la propiedad a definir tendrá una complejidad simple y será aplicada el mismo modelo utilizada en el ejemplo anterior. El fluente a definir especifica que el flujo permanecerá encendido desde el evento \textit{start} de la tarea \textit{Arrange\_Pickup\_Apm} y se apagará en el evento \textit{end} de la tares \textit{Produce\_Shipment\_Notice} de esta manera se establece una regla que asegura que el fluente estará encendido durante todo el proceso de transporte. Para el segundo fluente se establece que se encienda en el evento \textit{start} de la tarea \textit{Create\_Manifest} y se apagará en el evento \textit{end} de la tarea \textit{Produce Shipment\_Notice\_Manifest}.\\\newline
Se establece además la propiedad de que cuando ocurra el fluente B entonces el fluente A ya ocurrió. La figura 6.7 determina el escenario que se desea probar.

\begin{figure}[htp]
\centering
\includegraphics[scale=0.4]{images/propertyFluentViolated.png}
\caption{\textit{Modelo de estudio usando fluentes}}
\end{figure}

Luego, la figura 6.8 determina el resultado de la verificación de manera gráfica. En ella se puede visualizar la traza por la cual se cumple el fluente B pero no el fluente A. Esto es, existe una traza en la cual ocurre la tarea \textit{Produce\_Shipment\_Notice} pero no ocurrió la tarea \textit{Create Manifest}, de modo que la propiedad es falsa.

\begin{figure}[htp]
\centering
\includegraphics[scale=0.4]{images/resultPropertyFluentViolated.png}
\caption{\textit{Traza del violación de propiedad usando fluentes}}
\end{figure}

De igual manera se pueden definir sobre el mismo modelo propiedades que sean válidas. Un ejemplo de éstas sería indicar un fluente \textit{A} que se enciende en el evento \textit{start} de la tarea \textit{Arrange\_Pickup\_Apm} y se apagará en el evento \textit{end} de la tarea \textit{Produce\_Shipment\_Notice}. Y un fluente B en el que se enciende y se apaga en el evento \textit{start} y \textit{end} respectivamente de la tarea \textit{Produce\_Shipment\_Notice}. El resultado de esta propiedad es válida como lo muestra la figura 6.9.\\\newline

\begin{figure}[htp]
\centering
\includegraphics[scale=0.4]{images/resultValidProperty.png}
\caption{\textit{Resultado de una propiedad válida}}
\end{figure}

Este resultado expresa que siempre que se produzca la notificación del envío siempre hubo un acuerdo del lugar de la entrega. Esto resulta sencillo de definir gracias a la existencia de los fluentes ya que de lo contrario sería necesario tener en cuenta una combinación de eventos dentro de la fórmula caracterizando esta situación.
		 
\newpage
\chapter{Conclusiones y Trabajos Futuros}
Creemos que es muy importante poder analizar modelos de procesos de negocios mediante la verificación de propiedades ya que nos permite detectar errores en etapas tempranas de diseño. Construir un herramienta para poder brindar esta funcionalidad fue el objetivo de este proyecto. 
\\\newline
\emph{FLWA} fue producto de ese objetivo, permitiendo la definición de propiedades que se desean verificar en un modelo de proceso de negocio. Además, en caso de que la propiedad analizada no se cumpla, nuestra herramienta permite realizar un seguimiento de los eventos del proceso que llevan a su invalidez, permitiendo razonar y tener fundamentos para poder corregir el modelo o relajar la propiedad. En pos de tu utilización, tomamos como punto de partida modelos de procesos de negocios descriptos en el lenguaje \emph{YAWL}, aprovechando así las ventajas y herramientas que éste ofrece para la definición de \textit{workflows}. Mediante la inclusión de la lógica temporal de tiempo lineal (\emph{LTL}) y la lógica temporal de tiempo lineal con fluentes (\emph{FLTL}) se pudo proveer un mecanismo para la definición de propiedades. La utilización de estas lógicas como herramientas de análisis requieren modelos particulares, por ejemplo, sistemas de transición de estados. Por ello, como parte del proyecto se desarrolló \emph{yawl2fsp}, herramienta que traduce modelos \emph{YAWL} a un álgebra de procesos \emph{FSP} para luego ser compilado y analizado mediante la técnica de \textit{model checking}, en nuestro caso mediante \emph{LTSA}.
Todo este proceso es realizado mediante \emph{FLWA} quien permite la interacción con el usuario haciendo uso de funcionalidades gráficas facilitando el análisis de los procesos de negocio. Por último, el control de la comunicación entre las herramientas antes mencionadas, realzando los procesos de traducción necesarios y el análisis de los resultados por parte de \emph{LTSA}.
\\\newline

Personalmente creo que este trabajo fue un gran desafío. El hecho de incluir lógicas que desconocía y tecnologías como \textit{DECLARE} y \textit{yawl2FSP} que no he usado antes han logrado una complejidad adicional al proyecto y una satisfacción poder estudiarlas y explotar parte de las funcionalidades que éstas ofrecen. Por otra parte fue de gran importancia la comunicación con los desarrolladores de \emph{LTSA} y la herramienta mencionada anteriormente \textit{yawl2FSP}. Desarrollar una herramienta orientada a componentes visuales presentó complicaciones ya que fueron necesarios cálculos de coordenadas y optimizaciones necesarias para modelos complejos. El desarrollo mencionado incremento mis conocimientos en cada una de las etapas que participa en la creación del software. Creo que fue un proyecto que disfrute y logre sobrepasar los diferentes obstáculos presentados y aun mas por los conocimientos y experiencia adquirida.

\section{Trabajos futuros}
Los objetivos planteados fueron logrados, muchos de éstos llevaron un gran esfuerzo como el de comunicar la herramienta desarrollada con \emph{LTSA} ya que ésta sólo se encontraba en su versión gráfica. Por otra parte la representación de modelos \emph{YAWL} llevó un proceso de análisis para determinar una proceso eficiente.\\
Sin embargo en el marco de este proyecto quedaron diferentes ajustes o características que pueden lograr un mejor funcionamiento de \emph{FLWA}. Estas características pueden ser desarrolladas en el futuro.\\\newline
Dentro de las características se podrían mencionar, las siguientes:\\
Realizar una mejor impronta de las prestaciones gráficas que ofrece la herramienta, de manera de pulir ciertas funcionalidades y lograr la conformidad del usuario. Desarrollar un conjunto de comandos rápidos de manera de facilitar la definición de los fluentes y las propiedades; tomando como accesos rápidos la definición de los eventos que componen los fluentes antes definidos. De igual manera, incluir le opción de poder crear nuevas plantillas de manera automática desde la aplicación. Esto es, definir plantillas mediante un menú de opciones con la posibilidad de crear las formulas \emph{FLTL} que éstas contienen.
Por último se podría mejorar o reforzar el proceso de traducción de eventos y de esta manera lograr un mejor tratamiento de las interpretaciones sobre las trazas de ejecución.


\begin{thebibliography}{33}
\bibitem{declDirk}D. Fahland, J. Mendling, H. A. Reijers, B. Weber, M. Weidlich, S. Z.l, Declarative versus Imperative Process Modeling Languages: The Issue of Maintainability (inproceedings), Business Process Management Workshops, 2009

\bibitem{WestergaardMaggi2011}M. Westergaard, F. M. Maggi, Declare: A Tool Suite for Declarative Workflow Modeling and Enactment (inproceedings), BPM (Demos), 2011

\bibitem{GiannakopoulouMagee2003}D. Giannakopoulou, J. Magee, Fluent model checking for event-based systems (inproceedings), ESEC / SIGSOFT FSE, 2003

\bibitem{Schneider2004}K. Schneider, Verification of Reactive Systems: Formal Methods and Algorithms (Texts in Theoretical Computer Science. An EATCS Series), 2004

\bibitem{WorkflowPatterns2003}W. M. P. van der Aalst, A. H. M. ter Hofstede, B. Kiepuszewski, A. P. Barros, Workflow Patterns, Distributed and Parallel Databases, vol.14, 2003.

\bibitem{WorkflowPatterns2006}N. Russell, A.H.M. ter Hofstede, W.M.P. van der Aalst, N. Mulyar, Workflow Control-Flow Patterns: A Revised View, BPM Center Report BPM-06-22 , BPMcenter.org, 2006.

\bibitem{Ricci2012}N. Ricci, Verificación de Procesos de Negocios mediante Lógica de Fluentes, Universidad Nacional de Río Cuarto, 2012

\bibitem{BPMN20}OMG BPMN 2.0 - OMG Final Adopted Specification: http://www.omg.org/spec/BPMN/1.1/PDF/


\bibitem{WorkflowPattern}Workflow Patterns Initiative, http://www.workflowpatterns.com/patterns/, 2011

\bibitem{Petri2003} C. Girault and R. Valk, Petri nets for systems engineering - a guide to modeling, verification, and applications, Springer, 2003.

\bibitem{arrowhead} M. F. P. Rodrigues, http://ie.archive.ubuntu.com/disk1/disk1/sourceforge
/g/project/gr/graphs4students/src/graphs4students/gui/Edge.java

\bibitem{ltsaSource} J. Magee, J. Kramer, R. Chatley, S. Uchitel, H. Foster, Development a verification tool for concurrent systems called LTAS. 2006

\end{thebibliography}

\end{document}		